COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Thus the terminology "solvability" is apropos. Given ?M, an equation of the form
C00005 00003	These reduced forms of ?M1, ?M2, ?M3, and ?M4 all have the general form that:
C00013 00004	.SS(Some background on lattices)
C00025 00005	.begin "at|]" 
C00028 ENDMK
C⊗;
Thus the terminology "solvability" is apropos. Given ?M, an equation of the form
?M?X1#...#?Xk#=#?X can be solved for all terms ?X iff ?M is solvable.
We define a term with free variables as being solvable if there is a substitution 
of closed terms for its free variables such that the resulting closed term 
is solvable.

.GROUP;
Definition:
.BEGIN INDENT 5,5;
A term ?M is %3solvable%1 iff there is a head context⊗↓definition
{yon(R18)}← ∪C[#]∩ such that ∪C[M]∩ has a normal form.
.end
.apart

The concept of %3head normal form%1 provides a syntactic characterization
of the solvable terms. Consider again the unsolvable terms ?M1#≡#⊗d⊗d and
?M2#≡#⊗d∪(λx.xxx)∩, where ⊗d#≡#∪(λx.xx)∩.
Inspecting the reductions of these terms we find:

.begin indent 5,7;fill;
1) For ?M1 ≡ ⊗d⊗d, ?M1 reduces only to itself.

2) For ?M2 ≡ ⊗d∪(λx.xxx)∩, letting ∪T ≡ (λx.xxx)∩, every term to which ?M2
reduces is of the form ∪((λx.xxx)T)T#...#T∩ where ∪T∩ appears some finite
number of times (≥1).

.nofill
Consider also:
3) ?M3 ≡ ⊗d∪(λx.λy.xx)
       $r ∪(λx.xx)(λx.λy.xx)
       $r ∪(λx.λy.xx)(λx.λy.xx)
       $r ∪λy.(λx.λy.xx)(λx.λy.xx)
       $r ∪λy.λ?y1∪.(λx.λy.xx)(λx.λy.xx)
       $r ∪λy.λ?y1∪.λ?y2∪.(λx.λy.xx)(λx.λy.xx)∩
	etc.
Every term to which ?M3 reduces is of the form (after ?α-conversion):
	 ∪λy.λ?y1∪.λ?y2∪....?yn∪.(λx.λy.xx)(λx.λy.xx)∩

4) ?M4 ≡ ⊗d∪(λx.λy.xxx)∩, denoting ∪(λx.λy.xxx)∩ as ∪T∩', we have
       $r ∪T'T'
       $r ∪λy.(λx.λy.xxx)T'T'
       $r ∪λy∪.(λ?y1∪.(λx.λy.xxx)T'T')T'
	 ...∩

Every term to which ?M4 reduces is of the form (after ?α-conversion)
	∪λ?x1∪.(λ?x2∪.(...(λ?xn∪.(λx.λy.xxx)T'T') ...)T')T'∩
.end
These reduced forms of ?M1, ?M2, ?M3, and ?M4 all have the general form that:
either they consist of a single ?β-redex, or of a ?β-redex followed by a
finite number of arguments, or of a finite number of abstractions on one of these.
That is, they are of the form:
.begin center;

(%74%1)   ∪λ?x1?x2#...#?xn∪.((λx.M)N)?X1?X2 ... ?Xm∩ n≥0,m≥0.
.end
Such a term is called %3 a term not in head normal form%1 and the redex
∪(λx.M)N∩ is called its %3head redex%1.

The "paradoxical combinator" ∪Y%4λ%d ≡ λf.(λx.f(x x))(λx.f(x x))∩ is of the form
%74%1, but can be reduced to the term
∪λf.f((λx.f(x x))(λx.f(xx)))∩ which is not of the form %74%1. Also the terms:
.begin tabit1(30);select d;
\M ≡ λx.x(K)(A)
\N ≡ λx.x(KI)(A),
.end
where ?A is any term without a normal form are terms which have no normal forms, and
are not of  form %74%1. These three terms are not in normal form, but they are in
%3head normal form%1#(h.n.f.); that is, they are of the general form:
.begin center;select d;

(%75%d) λ?x1?x2 ...?xn∪.z∩ ?X1?X2 ...?Xk
.end
where n≥0, k≥0, ?z is a variable, and ?Xi are arbitrary terms.
Every term can be written in one of the forms %74%1 or %75%1 for suitable
n, k, ?Xi.

In %75%1 the variable ?z is known as the %3head variable%1, and  the term ?Xi
as its %3i%8th%3 main argument%1. Two head normal forms
are said to be %3similar%1 if they have the same head variable, the same number
of main arguments, and the same number of initial bound variables.
A term ?H in h.n.f. is said to be a %3head normal form of ?M%1 if ?M#$c#?H. 

The
reduction of ?M which always reduces the head redex is called the %3head reduction%1.
Analogously to normal  order reduction of terms to normal form, it
can be shown that a term has a head normal form iff its head
reduction terminates, and all head normal forms of a term are similar.
Thus we use head   reduction as  as  our computation scheme, being
interested only in whether or not a term has h.n.f. and not caring
about a normal form.
We shall see that it is consistent to equate all terms not having h.n.f.. We
know that computation will terminate precisely for those terms having a h.n.f., 
however, we have no decision procedure for recognizing whether or not an arbitrary
term has a h.n.f.

Comparing %75%1 with the structure of normal forms discussed earlier ({yon(R14)}),
we can see that in a head normal form the main arguments, ?X1,#,...,#?Xm
can be arbitrary terms, whereas a normal form requires that these
subterms also be in normal form. Thus a head normal form is a "weak" kind
of normal form which is in normal form only "at the first level".

It is easy to see that terms having a head normal form are solvable⊗↓The proof
of lemma 3, ({yon(R19)}), requires only that ?M have a %2head%1 normal form.←.
The converse can also be shown by syntactic means though we shall see a much easier
proof using Scott's lattice models⊗↓Theorem 17, Section 5.4←.

Thus we see that the unsolvable terms provide a more satisfactory analogue of
non-terminating programs than do terms not having a normal form.  Basically, the
reason for this is that unsolvability is preserved under application and composition,
that is, if ∪U∩ is unsolvable then so are ∪UX∩ and ∪U⊗x∪X∩⊗↓"?U composed
with ?X"← for all ?X, corresponding
to our intuition about non-terminating programs; that if, for example,
we perform two programs ⊗P1 and ⊗P2 in sequence and if ⊗P1 fails to terminate then
so does the sequence ⊗P1;⊗P2.
This behavior is not modelled by terms failing to have
normal forms, because, in general, the property of not having a normal form
is not preserved by application or by composition.

It was first shown by Barendregt that it is consistent to identify
all unsolvable terms⊗↓We can show this using Scott's models.←. From
a computational point of view it is certainly desirable to do so since they
behave alike.

We have considered what happens if terms are applied as functions; 
what if functions are applied to them? Even  for unsolvable terms we
can always obtain a normal form as result by using a constant function.
For example if ∪U∩ is unsolvable:
.begin center
∪(KI)U $r∪ I∩
.end
 But this method of using ?U as a subterm and obtaining a normal form
as a result is trivial, since ∪(KI)M#$r#∪I∩ for all terms ?M. In fact,
we can make a stronger statement.

%7LEMMA 4%1 If ?U is unsolvable, then, for all contexts ∪C[#]∩,
.begin indent 5,5
a) If ∪C[U]∩ has a normal form, the ∪C[M]∩ has the same normal form for all ?M.

b) If ∪C[U]∩ has a head normal form, then ∪C[M]∩ has a similar 
head normal form for all ?M.
.end

So the interpretation of unsolvable terms as being
"totally undefined" or "least defined" and as "containing no information" is a good one.
It should not be suprising therefore when we find that the unsolvable terms are exactly the terms
with value ⊗b is Scott's  model.
1:N~BO?7*βπ∂↑;K?Wv!β?9εcπSSN≠↔M$hRCK??∪π7Mε≠π;;␈!β∂?oβWS∃π;'S!εK''∪πKeεK;≠'vKS∃β}∪+↔∂'→9αSF)β7π&C↔7π&K∂π0hS↔;SO#'↔Mεkπ;'π+3πS.!βeπβK?∨⊗7Mβo+OQ1εK9βO}k∃βO.sO∃1ε∪∃β∪/#↔K7Ns↔⊃β↔IβS#.KH4+6K;'S*βπCC⊗{c'7∂#'?;≠Yβ?SF+K←'≡)βS#/∪∃β←␈+3⊃β⊗)β;=ε+≠≠↔∨#'[∃π;πeβ}1β∂π↔∪g';:β?WPhSS#∃ε≠?7C/#πS'}q9αSzβ↔∨NqβS=π≠↔∃βF{]β←*β∂π9ε∪W'3"β¬βSF+?Keε{→β≠Ns'S∀hSπCC⊗{c'7∂#'?9εCCK␈βK'π&)β≠?∩βS#∃πβK?+.≠Qβ?2β7πSF+7πSN≠π1β≡+7π;&K∂M1π;∃βπ⊗;W∀4W≠S↔An∪e7O&+Aβπ~β≠?3f{←MhhQ;↔>K9β'v#↔;Qβ)1Uo6K31lhQE%αnS#↔nS'∂∞aβO↔n;S'∨→βK↔∂+'K↔~↓#O?n)%↓Ns≠';O#∃	β}∪+↔∂'→β#π6K;≥βvyβ↔cεc'∂'"β≠';O#∀4+⊗+CK↔≡+;Sπ&K?98hP4)IJα';≠Ns'S∃ε{+↔∨#Mβ∂∞qβ;↔6+Iβ*βCK↔≡+;S↔"β?I↓⊗≠?7C/#↔⊃	ε+;S'⊗+3e↓FI;∃9bβ'9β6K;'S(h+S'n)%1β↔+Qβ?v)β∂πrβ∪↔S/∪7';*↓πCπ∪?c'nS'?w→	βSzβ←#π"βS#↔JβK↔πfceβπ⊗)84(hQM%α∂βCK?FK7πSN{;Mβ∂∪∃↓εKS'∞aβ?V+∂SM∩β←#'≡Aβ?;gIβ∨'6)βO?n)β?→π##∃βNs≠?KnS'?ph+π␈+QβSF)β∪π&	β?V+∂Q8hP4)QJα≠?Iε9β'v3';'&)β?V+∂Qβ&yβOS∞s⊃β¬ε≠#π;≡)β?→ε∪↔';:β∂?7π+Sπf)1β'"β7WO"β∂?;&'84Vs=β'v3?K7∂#'?9ε{[↔Iε;⊃β∞∪?[∃π##πQπ;#'∂Bβ'Mβ≡{;SπNs↔⊃βNqβ'S~β≠';O#∀4)FI;∃9bβ≠';O#↔3eπ∪↔CK/≠↔;S∞∪3∃%εCCK␈C'7π&K?;Mph);↔v 4*SF+O∃β}∪O↔K6S'?w→β3↔∞!βS=π##∃↓⊗+;W7/∪πS'}qβ7?&+1	β}1β∂?oβWSπ&K?9iε	β∪π&	β?V+∂Q?@4+∂∞qβ∃ε≠?7C/#↔⊃β↔Iβπ;J↓CK};Kπ5∩β←#'≡Aβ↔;.k↔Kπ&+Mβ¬π≠↔GW.s∂∃β}1βπCπ∪?c'nS'?w→β←#␈≠∀4+&{Sπ1α∪';≠␈∪7πSN{9β∂}sS↔;"⊃β'M;a84Ph*S#/→β∪π&	βOC∞≠↔Mβ}1β';&+K↔O"β≠?Iε	βS#.{Keβ}1β∂?oβWSπ&K?9β≡C?W3"β∃↓↔∪'∂#/⊃	4W##π9π##∃β≡{;[↔w#'?;∞aβ;?&K?9β}1β¬β&S¬β'KC∃mεK9βπ&#'S'}qβS=π##∃β/≠WOπb↓C↔⊗3↔∂SgH4+∪.3';↔"⊃β↔3.k↔;S~↓#';&+∨↔K~aβS?&1β≠.s∂S'}sM1β/#
%β␈+Iβ∪∂#¬βOε∂↔LhSO#?.c⊃βπg≠=β∂}sSπ'rβ?SBβCπK&Kπ1↓FI;∃9πβπKSN33eε#↔≠'v+⊃%β}∪+↔∂'_4+πv!β';6K;'S*β?+.≠SMβ∂→↓3Nk'SM∩β?→βεKS'∞aβ?V+∂SMrα←∃β/≠∃βSF)βS↔⊗h4)∃≡#?7πNq∃Eβ&yβK↔6+IβSzβOW∂Bβ∪πS
βOCπ≡+M9α>)β#π6)β¬β⊗+3πSN{9β?2βπCC⊗{c'7∂#'?8hS∪↔≠Ns↔⊃β}qβS#/≠∃β∪}kπ';≠Yβ←∃π;K'S+P4);⊗+∨'9ε≠↔;S/⊃l4(?A≤q;d4)v+;⊂4RCK↔π#Q∨aα∪πCC⊗{c'7∂#↔M	;e1β␈⊃∨aεKMβ3/≠MβSF9β?∩β↔GW∞c3eβ&+≠';.!βπM;e%β&yβ7↔∞q04+NsSW'&K[↔3JaβS#∂!∨eε≠?;S∞K;Mβ∞c1βSF)β';6{K7π&K?9β&CπQ?Aβ∪?/→84*≡c↔πKgI1βSFKMβK.cπS'}qβ'Mπ∪↔≠3/C'[∃bβSKπw≠'S'6)1βπv!βπ;&I7Ognk↔SKN→1βπv!βS#/→04+O→β¬βεKS'∞aβ?K&+Iβ?rβ?WIε#?7πNq84(hRS=β≡{7'v)βS#*β';≠␈∪7πSN{9β∨O3↔9β↔Iβ¬β≡+Q≡Bβ?→β∂βCK?FK7πSN{;Mβ>)β';'∪?∪W≡(4+SF)β?C/∪πS'}q∨0=A1βSF)↓∃OV{'9∃
β?→β&C∃βO/!≡abβ←#'≡Aβ'Mπ##∃βf+πOQπ+CC↔∩β?Wv!β?→h(≡aπ+;∪↔∩βS#∃πβπKSN1β?⊗#↔K'v984*O!β7W∨!β∂?w#π'9π##∃βNs≠?KnS'?rβ?→β∞c1β↔f+7↔;'→β?→:a↓#Js∃91εKQβ7/≠Qβ*βπ84W+CC↔∩β?Wv!%1β∞s⊃β'"βO#?.c⊃β;␈!β∂?w#π'9ε;eβ7+KS#/⊃β';6{K7π&K?9↓FI;∃9bβ'P4VkWOQε∪∃βSF)β3↔∂≠QβWπβ↔Iβ⊗{W;⊃Jp4(4T{WIβ&{7π'rβ'Mβ
β∂?7εc↔S∃εcπSSN≠∃βWv#↔Iβ&C∃βC∂∪S'πbβ?K∪ing π≤, which means
that πlπX exists for all subsets πX of the domain. We can define
some other lattice-theoretic concepts in terms of πl as follows:

.BEGIN "A" TURN OFF "{","}";
.BEGIN CENTER
πgπX = πl{πw : πwπ≤πx for all πxεπX}
.end
The %3meet%1 of the set πX⊂πD⊗↓"##" is a notation for 
"is a subset of".←, weakens the information of the elements of πX
giving a greatest lower bound.
.begin center;

⊗b = πl{ }  (or πgπD)
.end
"Bottom" gives no information, is totally undefined.
.begin center;

πt = πlπD   (or πg{ })
.end
"Top" gives too much information, it is overdefined to the point of being
inconsistent.
Note that ∀πxεπX,#πxπ≤πt and ⊗bπ≤πx.
.begin tabit1(15);group;

\πxπllπy = πl{πx, πy}
\πxπlgπy = πg{πx, πy}
\If πxπllπy = πt, then πx and πy are incomparable, i.e., not#πxπ≤πy and not#πyπ≤πx.
\If πxπlgπy = ⊗b, then πx and πy are incomparable, 
.end
.end "a"

We define a function πf:#πD#→#πD to be %3continuous%1 if 
f(πlπX)#=#πlπf(πX). And thus πxπ≤πy#=>πf(πx)π≤πf(πy).

.R22:
.group;
The lattice theoretic least fixpoint operator πY is defined:
.begin turn off "{","}";
.begin center;

πY(πf) = πLπf%8n%1(⊗b)
.end
and produces the least fixed points of contiouous functions.
A recursive function πf is typically defined to be some function, %gt%1, of the
identifier πf.  We define the 
sequence {πf%8n%1} by: πf%80%1#=#%gt%1(⊗b), πf%8n+1#=#%gt%1(πf%8n%1).
.end
.apart

The join (l.u.b.) πlπX of a set πX may properly be called the %3limit%1
of the set  only when πX is %3directed%1.  A subset πX of a domain is a 
%3directed set%1 iff every finite subset of πX has an upper bound in πX.
A directed set is %3interesting%1 if it does not contain its own least
upper bound.

A particular case of a directed set which it is generally sufficient to consider
is an infinite sequence of elements which form a chain.  A sequence πx0, πx1, πx2, ...
forms a %3chain%1 iff πx0π≤πx1π≤πx2π≤...
.begin turnoff "{", "}";
For chains, we generally write###πLπxn#for#πl{πxn | n≥0}
.end

The following properties are derived from these definitions:
.begin indent 7,7;nofill;group
L1. A set πX is directed iff it is non-empty and every pair of elements in πX has an upper 
    bound in πX.
L2. All interesting directed sets are infinite.
L3. Every countably infinite directed set contains a chain with the same limit.

.end
An element πx of a domain πD is a %3limit point%1 iff πx = πlπX for some 
interesting directed πX⊂πD.

The reason for introducing the idea of a basis is that, as mentioned before, we
want to restrict our attention to domains in which all elements are determined
by their finite (that is, finitely representable) approximations.  We can think
of a finite approximation as one which contains a finite amount of information.

Let πE⊂πD be the set of finitely representable elements of πD.  We wish to say 
that every πxεπD is the join of some set of finitely representable elements;
that is, there is some πE'⊂πE such that πx#=#πlπE'.  But when this holds, we
can include any element of πE which is π≤πx in πE' without changing its join, so,
for all πxεπD,
.begin turnoff "{", "}"; center

(*)         πx = πl{πe | πeεπE and πeπ≤πx}

.end
A set πE⊂πD such that (*) holds for all πxεπD is called a %3sub-basis%1 of 
πD.  We wish that πE consist only of finitely representable elements, which
requires that πE must be countable.  In fact, it is convenient to take this
requirement a step further.  Motivated by our intuition that the join of a
finite number of finite approximations still contains only a finite amount
of information, we define a basis.

A subset πE⊂πD is a %3basis%1 of πD iff it is a sub-basis and, for all finite
πE'⊂πE, πlπE'επE.  
.begin turnoff "{", "}";
Since the set  {πlπE' | πE'⊂πE, πE' finite} of finite joins of sub-basis
elements is countable whenever the sub-basis itself is countable, we
postulate that:  
.begin center;
Every domain has a countable basis.
.end
.end
This axiom effectively limits the size of a domain.  Since there are at most a
continuum number of subsets of a countable set, this implies that all domains
we consider have cardinality no larger than that of the real numbers.

The following properties are consequences of the definitions just given:  Let
πE be a basis for πD, then
.begin indent 10,10;nofill;turnoff "{", "}";
B1.  For all πxεπD,πx ≠ πt, the set {πe | πeεπE and πeπ≤πx} is directed.
B2.  If πxεπD is not a basis element, then πx is a limit point.
B3.  When πE is countable, every limit point πxεπD can be expressed as the limit of a
     chain of basis elements.
.end


.begin "at|]"; 
.at "|"⊂"%f)%1"⊃
.ss(The Models)
.begin indent 15, 15;
"The lambda-calculus is a curious language; one of my aims in life is to
make it somewhat less curious."
.nofill;
							D. Scott

.fill;
.end
We assume the existence of a complete lattice $D, with more than one
element, which is isomorpic to its own continuous function space [$D→$D].  (For
construction of the models represented by $D see Wadsworth [15] or Scott#[13].)
  We can express this isomorphism by two continuous functions
.begin center;

$f : $D → [$D → $D]
and
$y : [$D → $D] → $D
.end
.begin indent 10,20; nofill;
with the properties:
1) $y($f(πx)) = πx,    for all πxε$D
2) $f($y(πf)) = πf,    for all πfε[$D → $D]
.end

To interpret the ?λ-calculus in $D, we must first introduce some notation.
.begin nofill; tabit2 (15, 25);
\$I\for the set of all identifiers (variables)
\$X\for the set of all ?λ-terms
\$N\for the set of all environments
.end
and we shall use the meta-variable πd for a typical element of $D.  By an
%3environment πr we mean an association of values ("denotations") from $D
with all identifiers:
.begin center;
πr : $I → $D
.end
thus, $N is the set of all functions from $I to $D.  Given an environment in which
to interpret its free variables, the meaning of a term will be determined as
a composite of that of its immediate subterms by a mapping πV which takes
a term as argument and produces a function from $N to $Das result:

.begin center;
πV : $X → [$N →$D]⊗↓Sch⊗onfinkeling again!←
.end